Inference at * 
Iof proof for Lemma bnot-tt:


  a:. ((a) ~ tt)  (a ~ ff) 

latex

 by ((D (0)) 
CollapseTHENA (Auto)) 
CollapseTHEN (AutoBoolCase a) 

latex

C.

Definitions	left + right, Unit, P  Q, P & Q, x:A  B(x), x:AB(x), , s = t, b, A, b, x:A. B(x), , P  Q, t  T, s ~ t
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf